Skip to content

Updates posix_memalign to consider malloc may fail #5512

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Oct 8, 2020
Merged

Updates posix_memalign to consider malloc may fail #5512

merged 2 commits into from
Oct 8, 2020

Conversation

feliperodri
Copy link
Collaborator

Signed-off-by: Felipe R. Monteiro [email protected]

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@feliperodri feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 1, 2020
@feliperodri feliperodri self-assigned this Oct 1, 2020
@feliperodri feliperodri changed the title Update posix memalign Updates posix_memalign to consider malloc may fail Oct 1, 2020
martin-cs
martin-cs approved these changes Oct 1, 2020
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good; thanks.

@feliperodri feliperodri marked this pull request as ready for review October 1, 2020 21:45
@codecov
Copy link

codecov bot commented Oct 1, 2020 •
edited
Loading

Codecov Report

Merging #5512 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5512   +/-   ##
========================================
  Coverage    68.34%   68.34%           
========================================
  Files         1187     1187           
  Lines        98090    98090           
========================================
  Hits         67044    67044           
  Misses       31046    31046
Flag Coverage Δ
#cproversmt2 42.96% <ø> (ø)
#regression 65.49% <ø> (ø)
#unit 32.25% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 94fb414...d2eea3b. Read the comment docs.

hannes-steffenhagen-diffblue
hannes-steffenhagen-diffblue approved these changes Oct 5, 2020
View reviewed changes
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks OK to me, just don't quite understand the changes to one of these tests.

regression/cbmc-library/posix_memalign-01/test.desc
@@ -1,8 +1,8 @@
CORE
main.c
--pointer-check --bounds-check
--pointer-check --bounds-check --malloc-may-fail --malloc-fail-null
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't completely understand the changes for this test. You are changing the flags but not the expected output?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added the flags, so now the test considers malloc can fail. However, this doesn't change the expected output of this test, since it's resilient to a failed malloc. @hannes-steffenhagen-diffblue

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@feliperodri I'd recommend to reverse the changes here. Tests should be self contained and not contain flags that aren’t relevant for the test. This test is unrelated to --malloc-may-fail and hence shouldn’t use the flag.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@hannes-steffenhagen-diffblue I'll send a new PR that update these flags. I'll keep the failed regression test with the malloc flags and I'll remove them from the this test case.

@feliperodri
Copy link
Collaborator Author

Could I get one more review @tautschnig @kroening @chrisr-diffblue?

chrisr-diffblue
chrisr-diffblue approved these changes Oct 8, 2020
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks sensible, thanks!

@NlightNFotis NlightNFotis merged commit 1c42123 into diffblue:develop Oct 8, 2020
@feliperodri feliperodri deleted the update-posix_memalign branch October 8, 2020 14:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue approved these changes

@martin-cs martin-cs martin-cs approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees

@feliperodri feliperodri

Labels
aws Bugs or features of importance to AWS CBMC users
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@feliperodri @martin-cs @chrisr-diffblue @hannes-steffenhagen-diffblue @NlightNFotis